Left Termination of the query pattern
mergesort(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 185 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 349 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 6 ms)
        ↳25 QDP
        ↳26 MRRProof (⇔, 173 ms)
        ↳27 QDP
        ↳28 DependencyGraphProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 UsableRulesProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 QReductionProof (⇔, 0 ms)
        ↳33 QDP
        ↳34 QDPSizeChangeProof (⇔, 0 ms)
        ↳35 YES
    ↳36 PiDP
        ↳37 UsableRulesProof (⇔, 0 ms)
        ↳38 PiDP
        ↳39 PiDPToQDPProof (⇒, 0 ms)
        ↳40 QDP
        ↳41 QDPSizeChangeProof (⇔, 0 ms)
        ↳42 YES
    ↳43 PiDP
        ↳44 UsableRulesProof (⇔, 0 ms)
        ↳45 PiDP
        ↳46 PiDPToQDPProof (⇒, 0 ms)
        ↳47 QDP
        ↳48 Rewriting (⇔, 49 ms)
        ↳49 QDP
        ↳50 Rewriting (⇔, 0 ms)
        ↳51 QDP
        ↳52 QDPQMonotonicMRRProof (⇔, 551 ms)
        ↳53 QDP
        ↳54 DependencyGraphProof (⇔, 0 ms)
        ↳55 TRUE
    ↳56 PiDP
        ↳57 UsableRulesProof (⇔, 0 ms)
        ↳58 PiDP
        ↳59 PiDPToQDPProof (⇒, 0 ms)
        ↳60 QDP
        ↳61 Rewriting (⇔, 0 ms)
        ↳62 QDP
        ↳63 UsableRulesProof (⇔, 0 ms)
        ↳64 QDP
        ↳65 QReductionProof (⇔, 0 ms)
        ↳66 QDP
        ↳67 QDPOrderProof (⇔, 23 ms)
        ↳68 QDP
        ↳69 DependencyGraphProof (⇔, 0 ms)
        ↳70 TRUE

(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(X, []), .(X, [])).
mergesort(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(mergesort(X1s, Y1s), ','(mergesort(X2s, Y2s), merge(Y1s, Y2s, Ys)))).
split([], [], []).
split(.(X, Xs), .(X, Ys), Zs) :- split(Xs, Zs, Ys).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(le(X, Y), merge(Xs, .(Y, Ys), Zs)).
merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(gt(X, Y), merge(.(X, Xs), Ys, Zs)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Query: mergesort(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

splitA(.(X1, X2), .(X1, X3), X4) :- splitA(X2, X4, X3).
splitD(X1, X2, .(X1, X3), X4) :- splitA(X2, X4, X3).
mergesortE(.(X1, .(X2, X3)), X4) :- splitD(X1, .(X2, X3), X5, X6).
mergesortE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), mergesortE(X5, X7)).
mergesortE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, X7), mergesortE(X6, X8))).
mergesortE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, X7), ','(mergesortcE(X6, X8), mergeC(X7, X8, X4)))).
mergeC(.(X1, X2), .(X3, X4), .(X1, X5)) :- leF(X1, X3).
mergeC(.(X1, X2), .(X3, X4), .(X1, X5)) :- ','(lecF(X1, X3), mergeC(X2, .(X3, X4), X5)).
mergeC(.(X1, X2), .(X3, X4), .(X3, X5)) :- gtG(X1, X3).
mergeC(.(X1, X2), .(X3, X4), .(X3, X5)) :- ','(gtcG(X1, X3), mergeC(.(X1, X2), X4, X5)).
leF(s(X1), s(X2)) :- leF(X1, X2).
gtG(s(X1), s(X2)) :- gtG(X1, X2).
mergesortB(.(X1, .(X2, X3)), X4) :- splitD(X2, X3, X5, X6).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), mergesortB(.(X1, X6), X7)).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), mergesortE(X5, X8))).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), ','(mergesortcE(X5, X8), mergeC(X7, X8, X4)))).

Clauses:

splitcA([], [], []).
splitcA(.(X1, X2), .(X1, X3), X4) :- splitcA(X2, X4, X3).
mergesortcB([], []).
mergesortcB(.(X1, []), .(X1, [])).
mergesortcB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), ','(mergesortcE(X5, X8), mergecC(X7, X8, X4)))).
splitcD(X1, X2, .(X1, X3), X4) :- splitcA(X2, X4, X3).
mergesortcE([], []).
mergesortcE(.(X1, []), .(X1, [])).
mergesortcE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, X7), ','(mergesortcE(X6, X8), mergecC(X7, X8, X4)))).
mergecC([], X1, X1).
mergecC(X1, [], X1).
mergecC(.(X1, X2), .(X3, X4), .(X1, X5)) :- ','(lecF(X1, X3), mergecC(X2, .(X3, X4), X5)).
mergecC(.(X1, X2), .(X3, X4), .(X3, X5)) :- ','(gtcG(X1, X3), mergecC(.(X1, X2), X4, X5)).
lecF(s(X1), s(X2)) :- lecF(X1, X2).
lecF(0, s(X1)).
lecF(0, 0).
gtcG(s(X1), s(X2)) :- gtcG(X1, X2).
gtcG(s(X1), 0).

Afs:

mergesortB(x1, x2)  =  mergesortB(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
mergesortB_in: (b,f)
splitD_in: (b,b,f,f)
splitA_in: (b,f,f)
splitcD_in: (b,b,f,f)
splitcA_in: (b,f,f)
mergesortcB_in: (b,f)
mergesortcE_in: (b,f)
mergecC_in: (b,b,f)
lecF_in: (b,b)
gtcG_in: (b,b)
mergesortE_in: (b,f)
mergeC_in: (b,b,f)
leF_in: (b,b)
gtG_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, splitD_in_ggaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X2, X3, X5, X6)
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → U2_GGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U20_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U21_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U22_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_ggaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U8_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U9_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U10_GGA(X1, X2, X3, X4, X5, leF_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEF_IN_GG(X1, X3)
LEF_IN_GG(s(X1), s(X2)) → U16_GG(X1, X2, leF_in_gg(X1, X2))
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U12_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U13_GGA(X1, X2, X3, X4, X5, gtG_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTG_IN_GG(X1, X3)
GTG_IN_GG(s(X1), s(X2)) → U17_GG(X1, X2, gtG_in_gg(X1, X2))
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U15_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U23_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U24_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
mergesortB_in_ga(x1, x2)  =  mergesortB_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
splitA_in_gaa(x1, x2, x3)  =  splitA_in_gaa(x1)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergeC_in_gga(x1, x2, x3)  =  mergeC_in_gga(x1, x2)
leF_in_gg(x1, x2)  =  leF_in_gg(x1, x2)
gtG_in_gg(x1, x2)  =  gtG_in_gg(x1, x2)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
SPLITD_IN_GGAA(x1, x2, x3, x4)  =  SPLITD_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x2, x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5)  =  U20_GA(x1, x2, x3, x5)
U21_GA(x1, x2, x3, x4, x5, x6)  =  U21_GA(x1, x2, x3, x5, x6)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x1, x2, x3, x5, x6)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x1, x2, x3, x5, x6)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4, x5, x6)  =  U10_GGA(x1, x2, x3, x4, x6)
LEF_IN_GG(x1, x2)  =  LEF_IN_GG(x1, x2)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
U11_GGA(x1, x2, x3, x4, x5, x6)  =  U11_GGA(x1, x2, x3, x4, x6)
U12_GGA(x1, x2, x3, x4, x5, x6)  =  U12_GGA(x1, x2, x3, x4, x6)
U13_GGA(x1, x2, x3, x4, x5, x6)  =  U13_GGA(x1, x2, x3, x4, x6)
GTG_IN_GG(x1, x2)  =  GTG_IN_GG(x1, x2)
U17_GG(x1, x2, x3)  =  U17_GG(x1, x2, x3)
U14_GGA(x1, x2, x3, x4, x5, x6)  =  U14_GGA(x1, x2, x3, x4, x6)
U15_GGA(x1, x2, x3, x4, x5, x6)  =  U15_GGA(x1, x2, x3, x4, x6)
U23_GA(x1, x2, x3, x4, x5, x6)  =  U23_GA(x1, x2, x3, x5, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, splitD_in_ggaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X2, X3, X5, X6)
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → U2_GGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U20_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U21_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U22_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_ggaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U8_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U9_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U10_GGA(X1, X2, X3, X4, X5, leF_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEF_IN_GG(X1, X3)
LEF_IN_GG(s(X1), s(X2)) → U16_GG(X1, X2, leF_in_gg(X1, X2))
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U12_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U13_GGA(X1, X2, X3, X4, X5, gtG_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTG_IN_GG(X1, X3)
GTG_IN_GG(s(X1), s(X2)) → U17_GG(X1, X2, gtG_in_gg(X1, X2))
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U15_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U23_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U24_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
mergesortB_in_ga(x1, x2)  =  mergesortB_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
splitA_in_gaa(x1, x2, x3)  =  splitA_in_gaa(x1)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergeC_in_gga(x1, x2, x3)  =  mergeC_in_gga(x1, x2)
leF_in_gg(x1, x2)  =  leF_in_gg(x1, x2)
gtG_in_gg(x1, x2)  =  gtG_in_gg(x1, x2)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
SPLITD_IN_GGAA(x1, x2, x3, x4)  =  SPLITD_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x2, x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5)  =  U20_GA(x1, x2, x3, x5)
U21_GA(x1, x2, x3, x4, x5, x6)  =  U21_GA(x1, x2, x3, x5, x6)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x1, x2, x3, x5, x6)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x1, x2, x3, x5, x6)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4, x5, x6)  =  U10_GGA(x1, x2, x3, x4, x6)
LEF_IN_GG(x1, x2)  =  LEF_IN_GG(x1, x2)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
U11_GGA(x1, x2, x3, x4, x5, x6)  =  U11_GGA(x1, x2, x3, x4, x6)
U12_GGA(x1, x2, x3, x4, x5, x6)  =  U12_GGA(x1, x2, x3, x4, x6)
U13_GGA(x1, x2, x3, x4, x5, x6)  =  U13_GGA(x1, x2, x3, x4, x6)
GTG_IN_GG(x1, x2)  =  GTG_IN_GG(x1, x2)
U17_GG(x1, x2, x3)  =  U17_GG(x1, x2, x3)
U14_GGA(x1, x2, x3, x4, x5, x6)  =  U14_GGA(x1, x2, x3, x4, x6)
U15_GGA(x1, x2, x3, x4, x5, x6)  =  U15_GGA(x1, x2, x3, x4, x6)
U23_GA(x1, x2, x3, x4, x5, x6)  =  U23_GA(x1, x2, x3, x5, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 27 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
GTG_IN_GG(x1, x2)  =  GTG_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
LEF_IN_GG(x1, x2)  =  LEF_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4, x5, x6)  =  U11_GGA(x1, x2, x3, x4, x6)
U14_GGA(x1, x2, x3, x4, x5, x6)  =  U14_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)

The TRS R consists of the following rules:

lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4, x5, x6)  =  U11_GGA(x1, x2, x3, x4, x6)
U14_GGA(x1, x2, x3, x4, x5, x6)  =  U14_GGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U11_GGA(X1, X2, X3, X4, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)

The TRS R consists of the following rules:

lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U11_GGA(X1, X2, X3, X4, lecF_in_gg(X1, X3))

Strictly oriented rules of the TRS R:

gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + 2·x1 + x2   
POL(0) = 0   
POL(MERGEC_IN_GGA(x1, x2)) = 2·x1 + 2·x2   
POL(U11_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + 2·x3 + 2·x4 + x5   
POL(U14_GGA(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5   
POL(U40_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U41_gg(x1, x2, x3)) = x1 + x2 + x3   
POL(gtcG_in_gg(x1, x2)) = 1 + x1 + x2   
POL(gtcG_out_gg(x1, x2)) = x1 + x2   
POL(lecF_in_gg(x1, x2)) = 2·x1 + 2·x2   
POL(lecF_out_gg(x1, x2)) = 2·x1 + 2·x2   
POL(s(x1)) = 2·x1   

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U11_GGA(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)

The TRS R consists of the following rules:

lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))

The TRS R consists of the following rules:

lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(30) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))

The TRS R consists of the following rules:

gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(32) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

lecF_in_gg(x0, x1)
U40_gg(x0, x1, x2)

(33) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))

The TRS R consists of the following rules:

gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

gtcG_in_gg(x0, x1)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(34) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
    The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4

  • U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
    The graph contains the following edges 4 >= 2

(35) YES

(36) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(37) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(38) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(39) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X1, X2)) → SPLITA_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(41) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SPLITA_IN_GAA(.(X1, X2)) → SPLITA_IN_GAA(X2)
    The graph contains the following edges 1 > 1

(42) YES

(43) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(44) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(45) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(46) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(48) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3))) at position [3] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), splitcA_in_gaa(.(X2, X3))))

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), splitcA_in_gaa(.(X2, X3))))

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(50) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), splitcA_in_gaa(.(X2, X3)))) at position [3,2] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(52) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented dependency pairs:

U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2 + 2·x2   
POL(0) = 0   
POL(MERGESORTE_IN_GA(x1)) = 1 + 2·x1   
POL(U26_gaa(x1, x2, x3)) = 2 + 2·x3   
POL(U31_ggaa(x1, x2, x3)) = 1 + x3   
POL(U32_ga(x1, x2, x3, x4)) = 1   
POL(U33_ga(x1, x2, x3, x4, x5)) = 0   
POL(U34_ga(x1, x2, x3, x4, x5)) = 0   
POL(U35_ga(x1, x2, x3, x4)) = 0   
POL(U36_gga(x1, x2, x3, x4, x5)) = 0   
POL(U37_gga(x1, x2, x3, x4, x5)) = 0   
POL(U38_gga(x1, x2, x3, x4, x5)) = 0   
POL(U39_gga(x1, x2, x3, x4, x5)) = 0   
POL(U40_gg(x1, x2, x3)) = x3   
POL(U41_gg(x1, x2, x3)) = 1   
POL(U4_GA(x1, x2, x3, x4)) = 2 + 2·x4   
POL(U6_GA(x1, x2, x3, x4, x5)) = 1 + 2·x4   
POL([]) = 0   
POL(gtcG_in_gg(x1, x2)) = 2   
POL(gtcG_out_gg(x1, x2)) = 1   
POL(lecF_in_gg(x1, x2)) = x1   
POL(lecF_out_gg(x1, x2)) = 0   
POL(mergecC_in_gga(x1, x2)) = 0   
POL(mergecC_out_gga(x1, x2, x3)) = 0   
POL(mergesortcE_in_ga(x1)) = 1   
POL(mergesortcE_out_ga(x1, x2)) = 0   
POL(s(x1)) = 2 + x1   
POL(splitcA_in_gaa(x1)) = 1 + 2·x1   
POL(splitcA_out_gaa(x1, x2, x3)) = 1 + x2 + 2·x3   
POL(splitcD_in_ggaa(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = x3 + x4   

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(54) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(55) TRUE

(56) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x1, x2, x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6)  =  U28_ga(x1, x2, x3, x5, x6)
U29_ga(x1, x2, x3, x4, x5, x6)  =  U29_ga(x1, x2, x3, x5, x6)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U32_ga(x1, x2, x3, x4, x5)  =  U32_ga(x1, x2, x3, x5)
U33_ga(x1, x2, x3, x4, x5, x6)  =  U33_ga(x1, x2, x3, x5, x6)
U34_ga(x1, x2, x3, x4, x5, x6)  =  U34_ga(x1, x2, x3, x5, x6)
U35_ga(x1, x2, x3, x4, x5)  =  U35_ga(x1, x2, x3, x5)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5, x6)  =  U36_gga(x1, x2, x3, x4, x6)
lecF_in_gg(x1, x2)  =  lecF_in_gg(x1, x2)
s(x1)  =  s(x1)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lecF_out_gg(x1, x2)  =  lecF_out_gg(x1, x2)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x2, x3, x4, x6)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x1, x2, x3, x4, x6)
gtcG_in_gg(x1, x2)  =  gtcG_in_gg(x1, x2)
U41_gg(x1, x2, x3)  =  U41_gg(x1, x2, x3)
gtcG_out_gg(x1, x2)  =  gtcG_out_gg(x1, x2)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x2, x3, x4, x6)
U30_ga(x1, x2, x3, x4, x5)  =  U30_ga(x1, x2, x3, x5)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(57) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
splitcD_in_ggaa(x1, x2, x3, x4)  =  splitcD_in_ggaa(x1, x2)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x5)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U26_gaa(x1, x2, x3, x4, x5)  =  U26_gaa(x1, x2, x5)
splitcD_out_ggaa(x1, x2, x3, x4)  =  splitcD_out_ggaa(x1, x2, x3, x4)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(59) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(61) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, splitcD_in_ggaa(X2, X3)) at position [3] we obtained the following new rules [LPAR04]:

MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(63) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(65) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

splitcD_in_ggaa(x0, x1)

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(67) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(MERGESORTB_IN_GA(x1)) = x1   
POL(U19_GA(x1, x2, x3, x4)) = x4   
POL(U26_gaa(x1, x2, x3)) = 1 + x3   
POL(U31_ggaa(x1, x2, x3)) = 1 + x3   
POL([]) = 0   
POL(splitcA_in_gaa(x1)) = x1   
POL(splitcA_out_gaa(x1, x2, x3)) = x2 + x3   
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = 1 + x4   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

(68) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The set Q consists of the following terms:

U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(69) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(70) TRUE